M1, M2:MsgA, x:Id. M1  M2  (M2.ds(x) r M1.ds(x)) 

latex

Definitions	x:A. B(x), P  Q, M.ds(x), t.1, t  T, MsgA, M1  M2, Valtype(da;k), t.2, A c B, P & Q,
Lemmas	subtype-fpf-cap-top, top wf, Id wf, id-deq wf, ma-sub wf, msga wf